COMMENT ⊗   VALID 00010 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(load "combin.3")
C00004 00003	Bill,
C00005 00004	(REDUCIBLE '(Y F) '(F (Y F)))
C00006 00005	(reducible '(W (S (B W B)) F) '(S (B W B) F F))
C00007 00006	(reducible '(B W B F)
C00010 00007	(REDUCIBLE '(Y1 F) '(Y F))
C00012 00008	(reduce '((W (B f))(W (B f))))
C00013 00009	(reduce '(S (S ((K S) (S (K K)I)))(S (K S)(S (K I)(K I))) A B)) 
C00014 00010	Ok, then what's wrong with this? It is from page 41. 
C00020 ENDMK
C⊗;
(load "combin.3")
(alloc '(list 200000. 200000. ()))
(*rset (nouuo ()))
(load "combin.fas")
(reduce '((Z 0) F X)) 
(reduce '((Z 3) f x)) 
;(reduce '(S B (Z 8) f x)))
(reduce '(D2 x y (Z 0)))
(reduce '(D2 x y (Z (+ n 1))))
(reduce '(D2 x y (Z 1)))
(reducible '((Z 0) F X) '(X))
(reducible '(X) '((Z 0) F X))
(reducible '(Y f) '(f (Y f)))

(reducible '((Z (+ n 1))) '(S B (Z n))) 
(reduce '((Z (+ n 1))))
(reducible '(D2 x y (Z 0)) '(X))
(reducible '(D2 x y (Z (+ N 1))) '(Y))
(reducible '((W (B f))(W (B f))) 
	   '(W S (B W B) f))

((W (B F)) (W (B F))) 
- 
(W (B F) (W (B F))) 
(B W B F (W (B F))) 
(B W B F (B W B F)) 
(B W B F ((B W B) F)) 
((B W B) F ((B W B) F)) 
(S (B W B) (B W B) F) 
(W S (B W B) F) 
T 
(step apply1-reduction)
(sprinter (apply1-reduction '(K I F X)))
(SETQ PRINLEVEL 4 PRINGLENGTH ())
(reducible '((Z 0) F X) '(X))
(reducible '(x) '((Z 0) F X))
(X) 
(I X) 
(K I F X) 
((K I) F X) 
((Z 0) F X) 
T 
(reducible '((Z n)) '(S B (Z (- n 1))))
;HUNK4 STORAGE CAPACITY EXCEEDED
;BKPT GC-LOSSAGE
QUIT
* 
Bill,
I am reading Burge, and I think there is a bug in the proof that
Yf=f(Yf). Burge gives:

Yf = WS(BWB)f
   = S(BWB)ff
   = BWBf(BWBf)
   = W(Bf)(BWBf)
   = Bf(BWBf)(BWBf)
   = f(BWBf(BWBf))
   = f(Yf)

and I claim that going from the first to the second line is incorrect and
should be:

Yf = WS(BWB)f
   = S(BWB)(BWB)f
   = BWBf(BWBf)
   = W(Bf)(BWBf)
   = Bf(BWBf)(BWBf)
   = f(BWBf(BWBf))
   = f(Yf)

Does this jive with your understanding?
			-rpg-
(REDUCIBLE '(Y F) '(F (Y F)))
(Y F) 
(W S (B W B) F) 
(S (B W B) (B W B) F) 
(B W B F (B W B F)) 
(W (B F) (W (B F))) 
(B F (W (B F)) (W (B F))) 
(F (W (B F) (W (B F)))) 
(F (B W B F (W (B F)))) 
(F (B W B F (B W B F))) 
(F (Y F)) 
T 
(reducible '(W (S (B W B)) F) '(S (B W B) F F))
(reducible '(B W B F (B W B F)) '(S (B W B) F F))

(report)
366 nodes searched.
(W (S (B W B)) F) 
((S (B W B)) F F) 
(S (B W B) F F) 
4 nodes searched.
(reducible '(B W B F)
	   '(W (B F)))
(REDUCIBLE '(Y1 F) '(Y F))
(Y1 F) 
((W (B F)) (W (B F))) 
(W (B F) (W (B F))) 
((B F) (W (B F)) (W (B F))) 
(B F (W (B F)) (W (B F))) 
- 
(F ((W (B F)) (W (B F)))) 
(F (Y1 F)) 
T 
(Y1 F) 
((W (B F)) (W (B F))) 
(W (B F) (W (B F))) 
((B F) (W (B F)) (W (B F))) 
(B F (W (B F)) (W (B F))) 
(F ((W (B F)) (W (B F)))) 
- 
(F (W (B F) (W (B F)))) 
(F (B W B F (W (B F)))) 
(F (B W B F (B W B F))) 
(F (B W B F ((B W B) F))) 
(F ((B W B) F ((B W B) F))) 
(F (S (B W B) (B W B) F)) 
(F (W S (B W B) F)) 
(F (Y F)) 
T 
(Y1 F) 
((W (B F)) (W (B F))) 
- 
(W (B F) (W (B F))) 
(B W B F (W (B F))) 
(B W B F (B W B F)) 
(B W B F ((B W B) F)) 
((B W B) F ((B W B) F)) 
(S (B W B) (B W B) F) 
(W S (B W B) F) 
(Y F) 
T 
(reduce '((W (B f))(W (B f))))
(reduce '(D2 a b (Z (+ n 1))))
Reducing: (D2 A B (Z 0))
(D2 A B (Z 0)) 
 1 Processing: (Z 0)
 1 (Z 0) = (Z 0)
((Z 0) (K B) A)
((K I) (K B) A)
(K I (K B) A)
(I A)
(A)
(D2 A B (Z 0)) = (A)
(reduce '(D2 a b (Z (+ n 1))))
Reducing: (D2 A B (Z (+ N 1)))
(D2 A B (Z (+ N 1))) 
 1 Processing: (Z (+ N 1))
  2 Processing: (+ N 1)
  2 (+ N 1) = (+ N 1)
 1 (Z (+ N 1)) = (Z (+ N 1))
((Z (+ N 1)) (K B) A)
(S B (Z N) (K B) A)
(B (K B) ((Z N) (K B)) A)
((K B) (((Z N) (K B)) A))
 1 Processing: (K B)
 1 (K B) = (K B)
(K B (((Z N) (K B)) A))
(B)
(D2 A B (Z (+ N 1))) = (B)
T 
(reduce '(S (S ((K S) (S (K K)I)))(S (K S)(S (K I)(K I))) A B)) 
(reduce '(S (K S)(S (K I)(K I))(S (k i)(k i)) A B)) 
Ok, then what's wrong with this? It is from page 41. 
(S (K F) (S I I) x) is how I interpret the meaning of how 
λf.S(Kf)(SII) is supposed to be applied to x.

(reduce '(S (K F) (S I I) x))
Reducing: (S (K F) (S I I) X)
(S (K F) (S I I) X) 
((K F) X ((S I I) X))
(K F X ((S I I) X))
(F ((S I I) X))
 1 Processing: ((S I I) X)
  2 Processing: (S I I)
  2 (S I I) = (S I I)
 1 (S I I X)
 1 (I X (I X))
 1 (X (I X))
 1 ((S I I) X) = (X (I X))
 1 Processing: (X (I X))
  2 Processing: (I X)
  2 (X)
  2 (I X) = (X)
 1 (X X)
 1 (X (I X)) = (X X)
 1 Processing: (X X)
 1 (X X) = (X X)
(S (K F) (S I I) X) = (F (X X))
T 

Notice that this technology works like a champ on things like this:

(reduce '(D2 a b (Z (+ n 1))))
Reducing: (D2 A B (Z (+ N 1)))
(D2 A B (Z (+ N 1))) 
 1 Processing: (Z (+ N 1))
  2 Processing: (+ N 1)
  2 (+ N 1) = (+ N 1)
 1 (Z (+ N 1)) = (Z (+ N 1))
((Z (+ N 1)) (K B) A)
(S B (Z N) (K B) A)
(B (K B) ((Z N) (K B)) A)
((K B) (((Z N) (K B)) A))
 1 Processing: (K B)
 1 (K B) = (K B)
(K B (((Z N) (K B)) A))
(B)
(D2 A B (Z (+ N 1))) = (B)
T 

and:

(reduce '(D2 a b (Z 0)))
Reducing: (D2 A B (Z 0))
(D2 A B (Z 0)) 
 1 Processing: (Z 0)
 1 (Z 0) = (Z 0)
((Z 0) (K B) A)
((K I) (K B) A)
(K I (K B) A)
(I A)
(A)
(D2 A B (Z 0)) = (A)

I can test reducibility to:

(reducible '(D2 a b (Z (+ n 1))) '(B))
(D2 A B (Z (+ N 1))) 
((Z (+ N 1)) (K B) A) 
(S B (Z N) (K B) A) 
(B (K B) ((Z N) (K B)) A) 
((K B) (((Z N) (K B)) A)) 
(K B (((Z N) (K B)) A)) 
(K B ((Z N (K B)) A)) 
(K B (Z N (K B) A)) 
(B) 
22 nodes searched.
T 

So what am I doing wrong?
			-rpg-